#include "art.h"
#include <sstream>
#include <fstream>
#include <stdexcept>
int call_time;//debug

extern int exp(int x, int t);
extern string Int2String(int y);
extern string RecursiveSMTProp(Prop*, yicesl_context*, vector<Expr*>*);
extern string RecursiveSMTExpr(Expr*, yicesl_context*, vector<Expr*>*);
extern bool interfaceSMT(Prop*);

bool FindX1(Expr *, Expr *);
string StringProp(Prop*);
string StringExpr(Expr*);
void ART::AddNode(ArtNode *N){
   
}//add a node to ART
void PrintArtNode(ArtNode* artN){
    CFA cfa;
    if(typeid(*artN) == typeid(BinArtNode)){
        cfa.PrintProp(((BinNode*)(((BinArtNode*)artN)->cfa_node))->p); cout << endl;
        PrintArtNode(((BinArtNode*)artN)->next1);
        PrintArtNode(((BinArtNode*)artN)->next2);
    }
    else if(typeid(*artN) == typeid(UniArtNode)){
        cfa.PrintExpr(((UniNode*)(((UniArtNode*)artN)->cfa_node))->e1); cout << " = ";
        cfa.PrintExpr(((UniNode*)(((UniArtNode*)artN)->cfa_node))->e2); cout << endl;
        PrintArtNode(((BinArtNode*)artN)->next1);
    }
    else if(typeid(*artN) == typeid(BadArtNode)){
        cout << "Bad" << endl;
    }
    else if(typeid(*artN) == typeid(TermArtNode)){
        cout << "Terminal" << endl;
    }
    else{
    }
}

bool CompareExpr(Expr *e1, Expr *e2){
    bool r = true;
    if(typeid(*e1) == typeid(IntExpr)){
        if(typeid(*e2) == typeid(IntExpr)){
            if(((IntExpr*)e2)->i == ((IntExpr*)e1)->i){
                r = true; return r;
            }
            else{
                r = false; return r;
            }
        }
        else{
            r = false; return r;
        }
    }
    else if(typeid(*e1) == typeid(ArrayExpr)){
        if(typeid(*e2) == typeid(ArrayExpr)){
            if(strcmp(((ArrayExpr*)e2)->n, ((ArrayExpr*)e1)->n) == 0){
                if(CompareExpr(((ArrayExpr*)e2)->e, ((ArrayExpr*)e1)->e) == 0){
                    r = true; return r;
                }
                else{
                    r = false; return r;
                }
            }
            else{
                r = false; return r;
            }
        }
        else{
            r = false; return r;
        }
    }
    else if(typeid(*e1) == typeid(VarExpr)){
        if(typeid(*e2) == typeid(VarExpr)){
            if(strcmp(((VarExpr*)e1)->s, ((VarExpr*)e2)->s) == 0){
                r = true; return r;
            }
            else{
                r = false; return r;
            }
        }
        else{
            r = false; return r;
        }
    }
    else if(typeid(*e1) == typeid(BinExpr)){
        if(typeid(*e2) == typeid(BinExpr)){
            r = CompareExpr(((BinExpr*)e1)->e1, ((BinExpr*)e2)->e1) | CompareExpr(((BinExpr*)e1)->e2, ((BinExpr*)e2)->e2);
            return r;
        }
        else{
            r = false;
            return r;
        }
    }
    else{
    }
    return r;
}
bool CompareProp(Prop *p1, Prop *p2){
    bool r = false;
    if(typeid(*p1) == typeid(*p2)){
        if(typeid(*p1) == typeid(BoolProp)){
            if(((BoolProp*)p1)->b == ((BoolProp*)p2)->b){ return true; }
            else{ return false; }
        }
        else if(typeid(*p1) == typeid(NegProp)){
            return CompareProp(((NegProp*)p1)->p, ((NegProp*)p2)->p);
        }
        else if(typeid(*p1) == typeid(BinProp)){
            if(CompareProp(((BinProp*)p1)->p1, ((BinProp*)p2)->p1) && CompareProp(((BinProp*)p1)->p2, ((BinProp*)p2)->p2)){
                return true;
            }
            else{
                return false;
            }
        }
        else if(typeid(*p1) == typeid(InequProp)){
            if(FindX1(((InequProp*)p1)->e1, ((InequProp*)p2)->e1) &&  FindX1(((InequProp*)p1)->e2, ((InequProp*)p2)->e2)){  return true; }
            else{ return false; }
        }
    }
    else{ return false; }
    return r;
}
/*int ART::FindTimesMap(Expr *E){
    int times = -1;
    map<Expr*, int>::iterator it;
    pair<Expr*, int> p;
    //can't use M.find to find the times
    for(it=M.begin(); it!=M.end(); it++){
        if(CompareExpr(E, (*it).first)){
            (*it).second = (*it).second + 1; times = (*it).second; break;
        }
    }
    if(times == -1){
        p.first = E;
        p.second = 0;
        M.insert(p);
    }
    return times;
}*/
/*Expr* ART::ExchangeExpr(Expr *E){
    string rs;
    int times;
    Expr *E1, *E2, *E3;
    E1 = NULL; E2 = NULL; E3 = NULL;
    if(typeid(*E) == typeid(VarExpr)){
        times = FindTimesMap(E);
        E1 = new VarExpr;
        rs = ((VarExpr*)E)->s;
        rs = rs + "_" + Int2String(times);
        strcpy(((VarExpr*)E1)->s, (char*)(rs.c_str()));
    }
    else if(typeid(*E) == typeid(ArrayExpr)){
        times = FindTimesMap(E);
        E1 = new ArrayExpr;
        rs = ((ArrayExpr*)E)->n;
        rs = rs + "_" + Int2String(times); 
        strcpy(((ArrayExpr*)E1)->n, (char*)(rs.c_str()));
        E2 = ExchangeExpr(((ArrayExpr*)E)->e);
        ((ArrayExpr*)E1)->e = E2;
    }
    else if(typeid(*E) == typeid(BinExpr)){
        E2 = ExchangeExpr(((BinExpr*)E)->e1);
        E3 = ExchangeExpr(((BinExpr*)E)->e2);
        ((BinExpr*)E1)->e1 = E2;
        ((BinExpr*)E1)->e2 = E3;
    }
    else{
        E1 = E;
    }
    return E1;
}*/
/*Prop* ART::ExchangeProp(Prop *P){
    Prop *P1;
    P1 = NULL;
    if(typeid(*P) == typeid(BoolProp)){
        P1 = new BoolProp;
        ((BoolProp*)P1)->b = ((BoolProp*)P)->b;
    }
    else if(typeid(*P) == typeid(NegProp)){
        P1 = new NegProp;
        ((NegProp*)P1)->p = ExchangeProp(((NegProp*)P)->p);
    }
    else if(typeid(*P) == typeid(BinProp)){
        P1 = new BinProp;
        ((BinProp*)P1)->p1 = ExchangeProp(((BinProp*)P)->p1);
        ((BinProp*)P1)->p2 = ExchangeProp(((BinProp*)P)->p2);
    }
    else if(typeid(*P) == typeid(InequProp)){
        P1 = new InequProp;
        ((InequProp*)P1)->e1 = ExchangeExpr(((InequProp*)P1)->e1);
        ((InequProp*)P1)->e2 = ExchangeExpr(((InequProp*)P1)->e2);
    }
    else{
    }
    return P1;
}*/
bool FindX(Prop *phi, Expr *x){
    //CFA cfa;
    bool result;
    result = true;
    if(typeid(*phi) == typeid(BoolProp)){ result = false; }
    else if(typeid(*phi) == typeid(NegProp)){ 
        result = FindX(((NegProp*)phi)->p, x);
    }
    else if(typeid(*phi) == typeid(BinProp)){
        result = FindX(((BinProp*)phi)->p1, x) | FindX(((BinProp*)phi)->p2, x);
    }
    else if(typeid(*phi) == typeid(InequProp)){
        if(CompareExpr(((InequProp*)phi)->e1, x) || CompareExpr(((InequProp*)phi)->e2, x)){
            return true;
        }
        else{ return false; }
    }
    else{
    }
    return result;
}
bool FindX1(Expr *e, Expr *x){
    if(typeid(*e) == typeid(*x)){
        if(typeid(*e) == typeid(IntExpr)){
            if(((IntExpr*)e)->i == ((IntExpr*)x)->i){ return true; }
            else{ return false; }
        }
        else if(typeid(*e) == typeid(ArrayExpr)){
            if(strcmp(((ArrayExpr*)e)->n, ((ArrayExpr*)x)->n) == 0 && FindX1(((ArrayExpr*)e)->e, ((ArrayExpr*)x)->e)){ return true; }
            else{ return false; }
        }
        else if(typeid(*e) == typeid(VarExpr)){
            if(strcmp(((VarExpr*)e)->s, ((VarExpr*)x)->s) == 0){ return true; }
            else{ return false; }
        }
        else if(typeid(*e) == typeid(BinExpr)){
            if(FindX1(((BinExpr*)e)->e1, ((BinExpr*)x)->e1) && FindX1(((BinExpr*)e)->e1, ((BinExpr*)x)->e1)){ return true; }
            else{ return false; }
        }
        else{
        }
    }
    else{
        if(typeid(*e) == typeid(IntExpr)){ return false; }
        else if(typeid(*e) == typeid(ArrayExpr)){ return false; }
        else if(typeid(*e) == typeid(VarExpr)){ return false; }
        else if(typeid(*e) == typeid(BinExpr)){
            if(FindX1(((BinExpr*)e)->e1, x) || FindX1(((BinExpr*)e)->e2, x)){ return true; }
            else{ return false; }
        }
    }
    return false;
}
bool FindX2(Expr *e, Expr *x){
    if(typeid(*e) == typeid(*x)){
        if(typeid(*e) == typeid(IntExpr)){
            if(((IntExpr*)e)->i == ((IntExpr*)x)->i){ return true; }
            else{ return false; }
        }
        else if(typeid(*e) == typeid(ArrayExpr)){
            if(strcmp(((ArrayExpr*)e)->n, ((ArrayExpr*)x)->n) == 0 && FindX2(((ArrayExpr*)e)->e, ((ArrayExpr*)x)->e)){ return true; }
            else{ return false; }
        }
        else if(typeid(*e) == typeid(VarExpr)){
            if(strcmp(((VarExpr*)e)->s, ((VarExpr*)x)->s) == 0){ return true; }
            else{ return false; }
        }
        else if(typeid(*e) == typeid(BinExpr)){
            if(FindX2(((BinExpr*)e)->e1, ((BinExpr*)x)->e1) && FindX2(((BinExpr*)e)->e1, ((BinExpr*)x)->e1)){ return true; }
            else{ return false; }
        }
        else{
            return false;
        }
    }
    else{
        return false;
    }
}

Expr *ReplaceExpr(Expr *e, Expr *x){
    //CFA cfa;
    Expr *e_1;
    e_1 = NULL;
    string s;
    if(typeid(*e) == typeid(VarExpr)){
        if(CompareExpr(e, x)){
            e_1 = new VarExpr;
            s = ((VarExpr*)e)->s;
            s = s + "\'";
            strcpy(((VarExpr*)e_1)->s, s.c_str()); 
        }
        else{
            e_1 = e;
        }
        //cout << "Var " << ((VarExpr*)e_1)->s << endl;
    }
    else if(typeid(*e) == typeid(IntExpr)){
        e_1 = new IntExpr;
        ((IntExpr*)e_1)->i = ((IntExpr*)e)->i;
        //cout << "Int " << ((IntExpr*)e)->i << endl;
    }
    else if(typeid(*e) == typeid(ArrayExpr)){
        //cout << "Array" << endl;
        if(CompareExpr(e, x)){
            e_1 = new ArrayExpr;
            s = ((ArrayExpr*)e)->n;
            s = s + "\'";
            strcpy(((ArrayExpr*)e)->n, s.c_str());
        }
        else{
            e_1 = e;
        }
    }
    else if(typeid(*e) == typeid(BinExpr)){
        //cout << "Bin" << endl;
        e_1 = new BinExpr;
        ((BinExpr*)e_1)->e1 = ReplaceExpr(((BinExpr*)e)->e1, x);
        ((BinExpr*)e_1)->e2 = ReplaceExpr(((BinExpr*)e)->e2, x);
        ((BinExpr*)e_1)->op = ((BinExpr*)e)->op;
    }
    //cfa.PrintExpr(e_1); cout << endl;
    return e_1;
}
Prop* ReplaceProp(Prop* phi, Expr* e){
    //CFA cfa;
    Prop *phi_1;
    phi_1 = NULL;
    if(typeid(*phi) == typeid(BoolProp)){ 
        phi_1 = new BoolProp;
        ((BoolProp*)phi_1)->b = ((BoolProp*)phi)->b;
    }
    else if(typeid(*phi) == typeid(NegProp)){
        phi_1 = new NegProp;
        ((NegProp*)phi_1)->p = ReplaceProp(((NegProp*)phi)->p, e);
    }
    else if(typeid(*phi) == typeid(BinProp)){
        phi_1 = new BinProp;
        ((BinProp*)phi_1)->p1 = ReplaceProp(((BinProp*)phi)->p1, e);
        ((BinProp*)phi_1)->p2 = ReplaceProp(((BinProp*)phi)->p2, e);
        ((BinProp*)phi_1)->l = ((BinProp*)phi)->l;
    }
    else if(typeid(*phi) == typeid(InequProp)){
        phi_1 = new InequProp;
        if(CompareExpr(((InequProp*)phi)->e1, e)){
            ((InequProp*)phi_1)->e1 = ReplaceExpr(((InequProp*)phi)->e1, e);
        }
        else{
            ((InequProp*)phi_1)->e1 = ((InequProp*)phi)->e1;
        }
        if(CompareExpr(((InequProp*)phi)->e2, e)){
            ((InequProp*)phi_1)->e2 = ReplaceExpr(((InequProp*)phi)->e2, e);
        }
        else{
            ((InequProp*)phi_1)->e2 = ((InequProp*)phi)->e2;
        }
        ((InequProp*)phi_1)->p = ((InequProp*)phi)->p;
        //cfa.PrintProp(phi_1); cout << endl;
    }
    else{
    }
    return phi_1;
}
Prop* ART::ComputePost_Assign(Prop *phi, Expr *x, Expr *e){
    //CFA cfa;
    //cout << "test XXXX = " << StringProp(phi) << endl;
    Prop *phi_1, *x_1;
    phi_1 = new BinProp;
    x_1 = new InequProp;
    if(FindX(phi, x) == true){
        ((BinProp*)phi_1)->p1 = ReplaceProp(phi, x);
        ((BinProp*)phi_1)->l = And;
        ((InequProp*)x_1)->e1 = x;
        ((InequProp*)x_1)->e2 = ReplaceExpr(e, x);
        ((InequProp*)x_1)->p = Eq;
        ((BinProp*)phi_1)->p2 = x_1;
    }
    else{
        ((BinProp*)phi_1)->p1 = phi;
        ((BinProp*)phi_1)->l = And;
        ((InequProp*)x_1)->e1 = x;
        if(FindX1(e, x)){ ((InequProp*)x_1)->e2 = ReplaceExpr(e, x); }
        else{ ((InequProp*)x_1)->e2 = e; }
        ((InequProp*)x_1)->p = Eq;
        ((BinProp*)phi_1)->p2 = x_1;
    }
    //cfa.PrintProp(x_1); cout << endl;
    //cfa.PrintProp(((BinProp*)phi_1)->p1); cout << endl;
    //cfa.PrintProp(phi_1); cout << endl;
    return phi_1;
}
Prop* ART::ComputePost_Pred(Prop *phi, Prop *op){
    Prop *phi_1;
    phi_1 = new BinProp;
    ((BinProp*)phi_1)->p1 = phi;
    ((BinProp*)phi_1)->p2 = op;
    ((BinProp*)phi_1)->l = And;
    return phi_1;
}
Prop* CombineAndProp(Prop *p1, Prop *p2){
    Prop *p3;
    p3 = new BinProp;
    ((BinProp*)p3)->p1 = p1;
    ((BinProp*)p3)->p2 = p2;
    ((BinProp*)p3)->l = And;
    return p3;
}
Prop* ART::Gv(Prop *post, vector<Prop*> *predicate){
    //cout << "Post = " << StringProp(post) << endl;
    //CFA cfa;
    int i1, i2, i3;
    i1 = 0; i2 = 0; i3 = 0;
    int *t;
    Prop *phi, *neg, *com, *neg1;
    phi = NULL; neg = NULL; com = NULL;
    t = new int [ predicate->size() ];
    //~(~PostVP1) == Post ^ ~P1
    phi = new BinProp;
    neg = new NegProp;
    for(i1 = 0; i1 < (int)predicate->size(); i1++){
        //cout << "pred = " << StringProp((*predicate)[i1]) << endl;
        ((NegProp*)neg)->p = (*predicate)[i1];
        ((BinProp*)phi)->p1 = post;
        ((BinProp*)phi)->p2 = neg;
        ((BinProp*)phi)->l = And;
        //cout << "phi = " << StringProp(post) << endl;
        //if(call_time == 34){ cout << "phi 1= " << StringProp(phi) << endl; }
        //cout << "neg = " << StringProp(neg) << endl;
        if(interfaceSMT(phi)){ /*if(call_time == 34){ cout << "1" << endl;}*/ t[i1] = 1; continue; }
        ((BinProp*)phi)->p2 = (*predicate)[i1];
        //cout << "phi 2= " << StringProp(phi) << endl;
        //cfa.PrintProp(phi); cout << endl;
        if(interfaceSMT(phi)){ /*if(call_time == 34){ cout << "-1" << endl;}*/ t[i1] = -1; continue; }
        t[i1] = 0;
    }
    for(i1 = 0; i1 < (int)predicate->size(); i1++){
        //if(call_time == 34){ cout << "t = " << t[i1] << endl; }
        if(t[i1] == 1){
            i2 = i2 + 1;
            if(i2 == 1){
                com = (*predicate)[i1];
            }
            else{
                com = CombineAndProp(com, (*predicate)[i1]);
                //cout << StringProp(com) << endl;
            }
        }
        else if(t[i1] == -1){
            i2 = i2 + 1;
            neg = new NegProp;
            ((NegProp*)neg)->p = (*predicate)[i1];
            if(i2 == 1){
                //cout << "t[" << i1 << "]=" << t[i1] << " i2 = " << i2 << endl;
                com = neg;
                //cout << StringProp(neg) << endl;
            }
            else{
                com = CombineAndProp(com, neg);
            }
        }
        else{
            i3 = i3 + 1;
        }
    }
    if(i3 == (int)predicate->size()){
        com = new BoolProp;
        ((BoolProp*)com)->b = true;
    }
    delete [] t;
    return com;
}
bool ART::IsCover(ArtNode *N, Prop *P){
    //CFA cfa;
    map<Node*, vector<Prop*> >::iterator map_it;
    vector<Prop*>::iterator vec_it;
    map_it = CoverMap.find(((ArtNode*)N)->cfa_node);
    if(map_it == CoverMap.end()){ return false; }
    else{
        for(vec_it = (map_it->second).begin(); vec_it != (map_it->second).end(); vec_it++){
            //cfa.PrintProp(*vec_it); cout << "  --> "; cfa.PrintProp(P); cout << endl;
            if(CompareProp(*vec_it, P)){
                return true;
            }
        }
    }
    return false;
}
bool ART::IsEverCFANode(ArtNode *N){
    map<Node*, vector<Prop*> >::iterator map_it;
    map_it = CoverMap.find(((ArtNode*)N)->cfa_node);
    if(map_it == CoverMap.end()){ return false; }
    else{ return true; }
}
void ART::ADDphi2map(ArtNode *N, Prop *P){
    map<Node*, vector<Prop*> >::iterator map_it;
    map_it = CoverMap.find(((ArtNode*)N)->cfa_node);
    (map_it->second).push_back(P);
}
void ART::ADDpair2map(ArtNode *N, Prop *P){
    vector<Prop*> prop_inject;
    pair<Node*, vector<Prop*> > pair_inject;
    prop_inject.push_back(P);
    pair_inject.first = N->cfa_node;
    pair_inject.second = prop_inject;
    CoverMap.insert(pair<Node*, vector<Prop*> >(N->cfa_node, prop_inject));
}
bool ART::BuildART(ArtNode* N){
    //call_time = call_time + 1;
    //cout << "call time = " << call_time << endl;
    //sleep(1);
    bool result;
    result = true;
    int postFlag1, postFlag2;  //如果是1代表Post本身是true，若是0的話表示為false

    //建立一個art點
    if(typeid((*(N->cfa_node))) == typeid(BinNode)){
        //cout << "phi = " << endl; //cout << StringProp(((BinArtNode*)N)->phi) << endl;
        cout << "Printing Tag2 " << StringProp(((BinNode*)N->cfa_node)->p) << endl;
        ArtNode *T1, *T2;
        T1 = NULL; T2 = NULL;
        Prop *P1, *P2, *neg, *Pre1, *Pre2;
        P1 = ComputePost_Pred(((BinArtNode*)N)->phi, ((BinNode*)(N->cfa_node))->p);
        //cout << "P1 = " << StringProp(P1) << endl;
        if(interfaceSMT(P1)){  postFlag1 = 0; } //本來條件就是UNSAT
        else{ postFlag1 = 1; }
        //cout << "postFlag1 = " << postFlag1 << endl;
        Pre1 = Gv(P1, &(N->predicate));
        cout << "new phi = " << StringProp(Pre1) << endl;
            if(typeid(*((BinNode*)(N->cfa_node))->next1) == typeid(BinNode)){
                T1 = new BinArtNode;
                ((BinArtNode*)T1)->cfa_node = ((BinNode*)(N->cfa_node))->next1;
            }
            else if(typeid(*((BinNode*)(N->cfa_node))->next1) == typeid(UniNode)){
                T1 = new UniArtNode;
                ((UniArtNode*)T1)->cfa_node = ((BinNode*)(N->cfa_node))->next1;
            }
            else if(typeid(*((BinNode*)(N->cfa_node))->next1) == typeid(BadNode)){
                T1 = new BadArtNode;
                ((BadArtNode*)T1)->cfa_node = ((BinNode*)(N->cfa_node))->next1;
            }
            else if(typeid(*((BinNode*)(N->cfa_node))->next1) == typeid(TermNode)){
                T1 = new TermArtNode;
                ((TermArtNode*)T1)->cfa_node = ((BinNode*)(N->cfa_node))->next1;
            }
            else{
            }
            ((BinArtNode*)T1)->phi = Pre1;
            T1->predicate = N->predicate;
        if(postFlag1 == 1){
            ((BinArtNode*)N)->next1 = T1; 
        }
        else{ ((BinArtNode*)N)->next1 = NULL; }
        if(postFlag1 == 1){
            if(IsCover(T1, Pre1)){ //如果被Cover，就不用往下長
                if(typeid(*T1) == typeid(BinArtNode)){
                    ((BinArtNode*)T1)->next1 = NULL;
                    ((BinArtNode*)T1)->next2 = NULL;
                }
                else if(typeid(*T1) == typeid(UniArtNode)){
                    ((UniArtNode*)T1)->next1 = NULL;
                }
                else{
                }
                //return true;
            }
            else{                  //如果不是被Cover就必須修改map資料
                if(IsEverCFANode(T1)){  //如果CFA對應出現在map裡，就加入新的phi給second
                    ADDphi2map(T1, Pre1);
                }
                else{
                    ADDpair2map(T1, Pre1);
                }
                result = BuildART(T1);
            }
            if(result == false){ //碰到BadNode
                ((BinArtNode*)N)->next2 = NULL;
                todo.push_back(((BinArtNode*)N)->next2);
                return false;
            }
            else{ }
        }
        //}
        neg = new NegProp;
        ((NegProp*)neg)->p = ((BinNode*)(N->cfa_node))->p;
        P2 = ComputePost_Pred(((BinArtNode*)N)->phi, neg);
        if(interfaceSMT(P2)){ postFlag2 = 0; }
        else{ postFlag2 = 1; }
        Pre2 = Gv(P2, &(N->predicate));
            if(typeid(*((BinNode*)(N->cfa_node))->next2) == typeid(BinNode)){
                T2 = new BinArtNode;
                ((BinArtNode*)T2)->cfa_node = ((BinNode*)(N->cfa_node))->next2;
            }
            else if(typeid(*((BinNode*)(N->cfa_node))->next2) == typeid(UniNode)){
                T2 = new UniArtNode;
                ((UniArtNode*)T2)->cfa_node = ((BinNode*)(N->cfa_node))->next2;
            }
            else if(typeid(*((BinNode*)(N->cfa_node))->next2) == typeid(BadNode)){
                T2 = new BadArtNode;
                ((BadArtNode*)T2)->cfa_node = ((BinNode*)(N->cfa_node))->next2;
            }
            else if(typeid(*((BinNode*)(N->cfa_node))->next2) == typeid(TermNode)){
                T2 = new TermArtNode;
                ((TermArtNode*)T2)->cfa_node = ((BinNode*)(N->cfa_node))->next2;
            }
            else{
            }
            ((BinArtNode*)T2)->phi = Pre2;
            T2->predicate = N->predicate;
        if(postFlag2 == 1){
            ((BinArtNode*)N)->next2 = T2; 
        }
        else{ ((BinArtNode*)N)->next2 = NULL; }
            if(IsCover(T2, Pre2)){ //如果被Cover，就不用往下長
                //return true;
                if(typeid(*T2) == typeid(BinArtNode)){
                    ((BinArtNode*)T2)->next1 = NULL;
                    ((BinArtNode*)T2)->next2 = NULL;
                }
                else if(typeid(*T2) == typeid(UniArtNode)){
                    ((UniArtNode*)T2)->next1 = NULL;
                }
                else{
                }
            }
            else{	              //如果不是被Cover就必須修改map資料
                if(IsEverCFANode(T2)){  //如果CFA對應出現在map裡，就加入新的phi給second
                    ADDphi2map(T2, Pre2);
                }
                else{
                    ADDpair2map(T2, Pre2);
                }
                result = BuildART(T2);
            }
            if(result == false){ //碰到BadNode
                return false;
            }
            else{
                return true;
            }
        //}
    }
    else if(typeid(*(N->cfa_node)) == typeid(UniNode)){
        cout << "Printing Tag1 = " <<  StringExpr(((UniNode*)N->cfa_node)->e1) << "=" << StringExpr(((UniNode*)N->cfa_node)->e2) << endl;
        ArtNode *T1;
        T1 = NULL;
        Prop *P1, *Pre1;
        P1 = ComputePost_Assign(((UniArtNode*)N)->phi, ((UniNode*)(N->cfa_node))->e1, ((UniNode*)(N->cfa_node))->e2);
        //cout << "phi 1= " << StringProp(((UniArtNode*)N)->phi) << endl;
        //if(call_time == 34){ cout << "post 1= " << StringProp(P1) << endl; }
        //cout << "post 1= " << StringProp(P1) << endl;
        if(interfaceSMT(P1)){ return true; }//這邊有個問題，該回傳true or false
        Pre1 = Gv(P1, &(N->predicate));
        cout << "new phi = " << StringProp(Pre1) << endl;
        //if(call_time == 34){ exit(0); }
        if(typeid(*((UniNode*)(N->cfa_node))->next) == typeid(BinNode)){
            T1 = new BinArtNode;
            ((BinArtNode*)T1)->cfa_node = ((UniNode*)(N->cfa_node))->next;
        }
        else if(typeid(*((UniNode*)(N->cfa_node))->next) == typeid(UniNode)){
            T1 = new UniArtNode;
            ((UniArtNode*)T1)->cfa_node = ((UniNode*)(N->cfa_node))->next;
        }
        else if(typeid(*((UniNode*)(N->cfa_node))->next) == typeid(BadNode)){
            T1 = new BadArtNode;
            ((BadArtNode*)T1)->cfa_node = ((UniNode*)(N->cfa_node))->next;
        }
        else if(typeid(*((UniNode*)(N->cfa_node))->next) == typeid(TermNode)){
            T1 = new TermArtNode;
            ((TermArtNode*)T1)->cfa_node = ((UniNode*)(N->cfa_node))->next;
        }
        else{
            cout << "error" << endl;
        }
        T1->phi = Pre1;
        T1->predicate = N->predicate;
        ((UniArtNode*)N)->next1 = T1;
        if(IsCover(T1, Pre1)){ //如果被Cover，就不用往下長
            if(typeid(*T1) == typeid(BinArtNode)){
                ((BinArtNode*)T1)->next1 = NULL;
                ((BinArtNode*)T1)->next2 = NULL;
            }
            else if(typeid(*T1) == typeid(UniArtNode)){
                ((UniArtNode*)T1)->next1 = NULL;
            }
            else{
            }
            return true;
        }
        else{                 //如果不是被Cover就必須修改map資料
            if(IsEverCFANode(T1)){  //如果CFA對應出現在map裡，就加入新的phi給second
                ADDphi2map(T1, Pre1);
            }
            else{
                ADDpair2map(T1, Pre1);
            }
        }
        result = BuildART(T1);
        if(result == false){ //碰到BadNode
            return false;
        }
        else{
            return true;
        }
    }
    else if(typeid(*(N->cfa_node)) == typeid(BadNode)){
        return false;
    }
    else if(typeid(*(N->cfa_node)) == typeid(TermNode)){
        cout << "Term" << endl;
        return true;
    }
    else{
    }
    //跳出條件換成false Cover...
    return result;
}
void testpost1(ART art){
    Expr *e1, *e2, *e3, *e4, *e5;
    e1 = new VarExpr; e2 = new VarExpr; e3 = new IntExpr; e4 = new IntExpr; e5 = new IntExpr;
    Prop *t1, *t2, *t3, *t4, *t5, *t6;
    Prop *s, *s1;
    CFA cfa;
    vector<Prop*> Pred;
    t1 = new BinProp;
    t2 = new InequProp;
    t3 = new InequProp;
    strcpy(((VarExpr*)e1)->s, "a");
    strcpy(((VarExpr*)e2)->s, "b");
    ((IntExpr*)e3)->i = 0;
    ((IntExpr*)e4)->i = 1;
    ((InequProp*)t2)->e1 = e1;
    ((InequProp*)t2)->e2 = e3;
    ((InequProp*)t2)->p = GT;
    ((InequProp*)t3)->e1 = e2;
    ((InequProp*)t3)->e2 = e3;
    ((InequProp*)t3)->p = GT;
    ((BinProp*)t1)->p1 = t2;
    ((BinProp*)t1)->p2 = t3;
    ((BinProp*)t1)->l = And;//Fi origin
    //cfa.PrintProp(t2); cout << endl;
    //cfa.PrintProp(t3); cout << endl;
    //cfa.PrintProp(t1); cout << endl;
    t4 = new InequProp;
    t5 = new InequProp;
    ((InequProp*)t4)->e1 = e1;
    ((InequProp*)t4)->e2 = e4;
    ((InequProp*)t4)->p = GT;
    Pred.push_back(t4);
    ((InequProp*)t5)->e1 = e2;
    ((InequProp*)t5)->e2 = e3;
    ((InequProp*)t5)->p = GT; // Predicate assign
    Pred.push_back(t5);
    t6 = new InequProp;
    ((InequProp*)t6)->e1 = e1;
    ((InequProp*)t6)->e2 = e2;
    ((InequProp*)t6)->p = GT; // OP
    s = art.ComputePost_Pred(t1, t6);
    cfa.PrintProp(s);cout << endl;
    s1 = art.Gv(s, &Pred);
    cfa.PrintProp(s1);cout << endl;
}
void testpost2(ART art){
    Expr *e1, *e2, *e3, *e4, *e5;
    e1 = new VarExpr; e2 = new VarExpr; e3 = new IntExpr; e4 = new IntExpr; e5 = new BinExpr;
    Prop *t1, *t2, *t3, *t4, *t5, *t6;
    Prop *s, *s1;
    CFA cfa;
    vector<Prop*> Pred;
    t1 = new BinProp;
    t2 = new InequProp;
    t3 = new InequProp;
    strcpy(((VarExpr*)e1)->s, "a");
    strcpy(((VarExpr*)e2)->s, "b");
    ((IntExpr*)e3)->i = 0;
    ((IntExpr*)e4)->i = 1;
    ((InequProp*)t2)->e1 = e1;
    ((InequProp*)t2)->e2 = e3;
    ((InequProp*)t2)->p = GT;
    ((InequProp*)t3)->e1 = e2;
    ((InequProp*)t3)->e2 = e3;
    ((InequProp*)t3)->p = GT;
    ((BinProp*)t1)->p1 = t2;
    ((BinProp*)t1)->p2 = t3;
    ((BinProp*)t1)->l = And;//Fi origin
    //cfa.PrintProp(t2); cout << endl;
    //cfa.PrintProp(t3); cout << endl;
    //cfa.PrintProp(t1); cout << endl;
    t4 = new InequProp;
    t5 = new InequProp;
    ((InequProp*)t4)->e1 = e1;
    ((InequProp*)t4)->e2 = e4;
    ((InequProp*)t4)->p = GT;
    Pred.push_back(t4);
    ((InequProp*)t5)->e1 = e2;
    ((InequProp*)t5)->e2 = e3;
    ((InequProp*)t5)->p = GT; // Predicate assign
    Pred.push_back(t5);
    t6 = new InequProp;
    ((BinExpr*)e5)->e1 = e1;
    ((BinExpr*)e5)->op = Plus;
    ((BinExpr*)e5)->e2 = e4;// OP
    //cfa.PrintExpr(e1); cout << endl;
    //cfa.PrintExpr(e4); cout << endl;
    //cfa.PrintExpr(e5); cout << endl;
    s = art.ComputePost_Assign(t1, e1, e5);
    cfa.PrintProp(s);cout << endl;
    s1 = art.Gv(s, &Pred);
    cfa.PrintProp(s1);cout << endl;
}
void testpost3(ART art){
    Expr *e1, *e2, *e3, *e4, *e5;
    e1 = new VarExpr; e2 = new VarExpr; e3 = new IntExpr; e4 = new IntExpr; e5 = new BinExpr;
    Prop *t1, *t2, *t3, *t4, *t5, *t6;
    Prop *s, *s1;
    CFA cfa;
    vector<Prop*> Pred;
    t1 = new BinProp;
    t2 = new InequProp;
    t3 = new InequProp;
    strcpy(((VarExpr*)e1)->s, "a");
    strcpy(((VarExpr*)e2)->s, "b");
    ((IntExpr*)e3)->i = 0;
    ((IntExpr*)e4)->i = 1;
    ((InequProp*)t2)->e1 = e1;
    ((InequProp*)t2)->e2 = e3;
    ((InequProp*)t2)->p = GT;
    ((InequProp*)t3)->e1 = e2;
    ((InequProp*)t3)->e2 = e3;
    ((InequProp*)t3)->p = GT;
    ((BinProp*)t1)->p1 = t2;
    ((BinProp*)t1)->p2 = t3;
    ((BinProp*)t1)->l = And;//Fi origin
    //cfa.PrintProp(t2); cout << endl;
    //cfa.PrintProp(t3); cout << endl;
    //cfa.PrintProp(t1); cout << endl;
    t4 = new InequProp;
    t5 = new InequProp;
    ((InequProp*)t4)->e1 = e1;
    ((InequProp*)t4)->e2 = e4;
    ((InequProp*)t4)->p = GT;
    Pred.push_back(t4);
    ((InequProp*)t5)->e1 = e2;
    ((InequProp*)t5)->e2 = e3;
    ((InequProp*)t5)->p = GT; // Predicate assign
    Pred.push_back(t5);
    t6 = new InequProp;
    ((BinExpr*)e5)->e1 = e2;
    ((BinExpr*)e5)->op = Plus;
    ((BinExpr*)e5)->e2 = e4;// OP
    //cfa.PrintExpr(e1); cout << endl;
    //cfa.PrintExpr(e4); cout << endl;
    //cfa.PrintExpr(e5); cout << endl;
    s = art.ComputePost_Assign(t1, e1, e5);
    cfa.PrintProp(s);cout << endl;
    s1 = art.Gv(s, &Pred);
    cfa.PrintProp(s1);cout << endl;
}
void testpost4(ART art){
    Expr *e1, *e2, *e3, *e4, *e5, *e6, *e7, *e8, *e9;
    e1 = new VarExpr; e2 = new VarExpr; e3 = new IntExpr; e4 = new IntExpr; e5 = new BinExpr;
    e6 = new IntExpr; e7 = new IntExpr; e8 = new IntExpr; e9 = new VarExpr;
    Prop *t1, *t2, *t3, *t4, *t5, *t6, *t7, *t8, *t9;
    Prop *s, *s1;
    CFA cfa;
    vector<Prop*> Pred;
    t1 = new BinProp;
    t2 = new InequProp;
    t3 = new InequProp;
    t7 = new InequProp;
    t8 = new InequProp;
    t9 = new InequProp;
    strcpy(((VarExpr*)e1)->s, "a");
    strcpy(((VarExpr*)e2)->s, "b");
    strcpy(((VarExpr*)e9)->s, "c");
    ((IntExpr*)e3)->i = 0;
    ((IntExpr*)e4)->i = 1;
    ((IntExpr*)e6)->i = 5;
    ((IntExpr*)e7)->i = 6;
    ((IntExpr*)e8)->i = 7;
    ((InequProp*)t2)->e1 = e1;
    ((InequProp*)t2)->e2 = e2;
    ((InequProp*)t2)->p = GT;
    ((InequProp*)t3)->e1 = e2;
    ((InequProp*)t3)->e2 = e6;
    ((InequProp*)t3)->p = GT;
    ((BinProp*)t1)->p1 = t2;
    ((BinProp*)t1)->p2 = t3;
    ((BinProp*)t1)->l = And;//Fi origin
    //cfa.PrintProp(t2); cout << endl;
    //cfa.PrintProp(t3); cout << endl;
    //cfa.PrintProp(t1); cout << endl;
    t4 = new InequProp;
    t5 = new InequProp;
    ((InequProp*)t4)->e1 = e9;
    ((InequProp*)t4)->e2 = e3;
    ((InequProp*)t4)->p = GT;
    Pred.push_back(t4);
    ((InequProp*)t5)->e1 = e1;
    ((InequProp*)t5)->e2 = e2;
    ((InequProp*)t5)->p = GT; 
    Pred.push_back(t5);
    ((InequProp*)t7)->e1 = e2;
    ((InequProp*)t7)->e2 = e6;
    ((InequProp*)t7)->p = GT;  
    Pred.push_back(t7);
    ((InequProp*)t8)->e1 = e1;
    ((InequProp*)t8)->e2 = e8;
    ((InequProp*)t8)->p = GT;  
    Pred.push_back(t8);
    ((InequProp*)t9)->e1 = e2;
    ((InequProp*)t9)->e2 = e7;
    ((InequProp*)t9)->p = GT; // Predicate 
    Pred.push_back(t9);
    t6 = new InequProp;
    ((BinExpr*)e5)->e1 = e2;
    ((BinExpr*)e5)->op = Plus;
    ((BinExpr*)e5)->e2 = e4;// OP
    //cfa.PrintExpr(e1); cout << endl;
    //cfa.PrintExpr(e4); cout << endl;
    //cfa.PrintExpr(e5); cout << endl;
    s = art.ComputePost_Assign(t1, e2, e5);
    cfa.PrintProp(s); cout << endl;
    s1 = art.Gv(s, &Pred);
    cfa.PrintProp(s1); cout << endl;
}

/*string ART::RecursiveProp(Prop* p){
    string r;
    if(typeid(*p) == typeid(BoolProp)){
        if(((BoolProp*)p)->b == true){ r = "true";  }
        else{ r = "false"; }
    }
    else if(typeid(*p) == typeid(NegProp)){
        r = "~ " + RecursiveProp(((NegProp*)p)->p);
    }
    else if(typeid(*p) == typeid(BinProp)){
        if(((BinProp*)p)->l == And){ r = "& ["; }
        else{ r = "| [";  }
        r = r + " " + RecursiveProp(((BinProp*)p)->p1);
        r = r + " " + RecursiveProp(((BinProp*)p)->p2); 
        r = r + " ];";
    }
    else if(typeid(*p) == typeid(InequProp)){
        if(((InequProp*)p)->p == LT){
           r = "~ <=";
            r = r + " " + RecursiveExpr(((InequProp*)p)->e2);
            r = r + " " + RecursiveExpr(((InequProp*)p)->e1);
        }
        else if(((InequProp*)p)->p == GT){ 
            r = "~ <=";
            r = r + " " + RecursiveExpr(((InequProp*)p)->e1);
            r = r + " " + RecursiveExpr(((InequProp*)p)->e2);
        }
        else{ 
            r = "= ";
            r = r + " " + RecursiveExpr(((InequProp*)p)->e1);
            r = r + " " + RecursiveExpr(((InequProp*)p)->e2);
        }
    }
    return r;
}*/
/*string ART::RecursiveExpr(Expr* e){
    string r;
    if(typeid(*e) == typeid(IntExpr)){
        r = Int2String(((IntExpr*)e)->i);
    }
    else if(typeid(*e) == typeid(ArrayExpr)){
        r = ((ArrayExpr*)e)->n ;
        r = r + "[ ";
        r = r + RecursiveExpr(((ArrayExpr*)e)->e);
        r = r + " ]";
    }
    else if(typeid(*e) == typeid(VarExpr)){
        r = ((VarExpr*)e)->s;
    }
    else if(typeid(*e) == typeid(BinExpr)){
        if(((BinExpr*)e)->op == Plus){ r = "+ "; }
        else if(((BinExpr*)e)->op == Minus){ r = "- "; }
        else if(((BinExpr*)e)->op == Multi){ r = "* "; }
        else if(((BinExpr*)e)->op == Divide){ r = "/ "; }
        r = r + RecursiveExpr(((BinExpr*)e)->e1);
        r = r + " " + RecursiveExpr(((BinExpr*)e)->e2);
    }
    else{
    }
    return r;
}*/
/*string ART::RecursiveBuildPF(ArtNode* an, Node* cfaNode, vector<Prop*> *P, vector<int> *BP){
    //leave recursive constraints: 1. without nexxt 2. bad node 3. cover
    string s;
    call_time = call_time + 1;
    PostType Fi;
    //generate the artNode
    if(typeid(*cfaNode) == typeid(UniNode)){
        an = new UniArtNode;
        an->predicate = *P;
        an->Bpredicate = *BP;
        if(cfaNode->before.size() == 0){ an->Bpredicate[0] = 1; } // initial node
    }
    else if(typeid(*cfaNode) == typeid(BinNode)){
        an = new BinArtNode;
        an->predicate = *P;
        an->Bpredicate = *BP;
        if(cfaNode->before.size() == 0){ an->Bpredicate[0] = 1; } // initial node
    }
    else if(typeid(*cfaNode) == typeid(BadNode)){
        an = new BadArtNode;
        an->predicate = *P;
        an->Bpredicate = *BP;
        if(cfaNode->before.size() == 0){ an->Bpredicate[0] = 1; } // initial node
    }
    else if(typeid(*cfaNode) == typeid(TermNode)){
        an = new TermArtNode;
        an->predicate = *P;
        an->Bpredicate = *BP;
        if(cfaNode->before.size() == 0){ an->Bpredicate[0] = 1; } // initial node
    }

    Fi = CountPost(an, cfaNode, P, &(an->Bpredicate));
    if(typeid(*cfaNode) == typeid(UniNode)){
        s = s + "= ";
        s = s + RecursiveExpr(((UniNode*)cfaNode)->e1);
        s = s + " " + RecursiveExpr(((UniNode*)cfaNode)->e2) + "\n";
        s = s + RecursiveBuildPF(an, ((UniNode*)cfaNode)->next, P, BP);
    }
    else if(typeid(*cfaNode) == typeid(BinNode)){
        s = s + RecursiveProp(((BinNode*)cfaNode)->p) + "\n";
        s = s + RecursiveBuildPF(an, ((BinNode*)cfaNode)->next1, P, BP);
        s = s + "~ " + RecursiveProp(((BinNode*)cfaNode)->p) + "\n";
        s = s + RecursiveBuildPF(an, ((BinNode*)cfaNode)->next2, P, BP);
    }
    else if(typeid(*cfaNode) == typeid(BadNode)){
        return s;
    }
    else if(typeid(*cfaNode) == typeid(TermNode)){
        return s;
    }
    else{
        cout << "error!!!" << endl;
    }
    return s;
}*///

/*string ART::CreatePredicate(ArtNode* an, Node* initNode, vector<Prop*> *P, vector<int> *BP){
    string pathFormula;
    pathFormula = RecursiveBuildPF(an, initNode, P, BP);
    return pathFormula;
}*/
/*void ART::RecursiveBuildArt(Node *N, set<int> *s){
    //if(s->find(N) != s->end()){ return; }
    ArtNode *an = NULL;
    string s1;
    vector<int> BP; BP.clear();
    vector<Prop*> P; P.clear();
    map<Node*, vector<ArtNode*> > recordForCovered;
    Prop *startPredicate = new BoolProp;
    ((BoolProp*)startPredicate)->b = true;
    P.push_back(startPredicate);// initial the true
    BP.push_back(0);		// initial the bool value = unknown
    s1 = CreatePredicate(an, N, &P, &BP);
    cout << "Generated the Predicate!!!" << endl;
}*/
int ART::FindXTimes(Expr* e){
    map<Expr*, int>::iterator it;
    for(it = UseTimes.begin(); it != UseTimes.end(); it++){
        if(FindX2(e, it->first)){
            return it->second;
        }
    }
    return 0;
}
string StringOPType(OPType l){
    string s;
    if(l == Plus){ s = "+"; }
    else if(l == Minus){ s = "-"; }
    else if(l == Multi){ s = "*"; }
    else if(l == Divide){ s = "/"; }
    else{ }
    return s;
}
string StringLogicType(LogicType l){
    string s;
    if(l == And){ s = "& "; }
    else{ s = "| "; }
    return s;
}
string StringPropType(PropType l){
    string s;
    if(l == GT){ s = ">"; }
    else if(l == LT){ s = "<"; }
    else{ s = "="; }
    return s;
}
string StringExpr(Expr* e){
    string s;
    if(typeid(*e) == typeid(IntExpr)){
        s = Int2String(((IntExpr*)e)->i);
    }
    else if(typeid(*e) == typeid(VarExpr)){
        s = ((VarExpr*)e)->s;
    }
    else if(typeid(*e) == typeid(ArrayExpr)){
        s = ((ArrayExpr*)e)->n;
        s = s + "[ ";
        s = s + StringExpr(((ArrayExpr*)e)->e);
        s = s + " ]";
    }
    else if(typeid(*e) == typeid(BinExpr)){
        s = StringOPType(((BinExpr*)e)->op);
        s = s + " " + StringExpr(((BinExpr*)e)->e1);
        s = s + " " + StringExpr(((BinExpr*)e)->e2);
    }
    else{
    }
    return s;
}
string ART::StringExprWithTimes(Expr* e){
    string s1, s2, s3;
    if(typeid(*e) == typeid(IntExpr)){
        s3 = Int2String(((IntExpr*)e)->i);
    }
    else if(typeid(*e) == typeid(VarExpr)){
        s3 = ((VarExpr*)e)->s;
        s3 = s3 + "_";
        s3 = s3 + Int2String(FindXTimes(e));
    }
    else if(typeid(*e) == typeid(ArrayExpr)){
        s3 = ((ArrayExpr*)e)->n;
        s3 = s3 + "[ ";
        s3 = s3 + StringExprWithTimes(((ArrayExpr*)e)->e);
        s3 = s3 + " ]";
        s3 = s3 + "_" + Int2String(FindXTimes(e));
    }
    else if(typeid(*e) == typeid(BinExpr)){
        s3 = StringOPType(((BinExpr*)e)->op);
        s3 = s3 + " " + StringExprWithTimes(((BinExpr*)e)->e1);
        s3 = s3 + " " + StringExprWithTimes(((BinExpr*)e)->e2);
    }
    else{
    }
    return s3;
}
string StringProp(Prop* p){
    string s;
    if(typeid(*p) == typeid(BoolProp)){
        if(((BoolProp*)p)->b == true){ s = "true"; }
        else{ s = "false"; }
    }
    else if(typeid(*p) == typeid(NegProp)){
        s = "~ ";
        s = s + StringProp(((NegProp*)p)->p);
    }
    else if(typeid(*p) == typeid(BinProp)){
        s = StringLogicType(((BinProp*)p)->l);
        s = s + " " + StringProp(((BinProp*)p)->p1);
        s = s + " " + StringProp(((BinProp*)p)->p2);
    }
    else if(typeid(*p) == typeid(InequProp)){
        if(((InequProp*)p)->p == LT){
            s = "<";
            s = s + " " + StringExpr(((InequProp*)p)->e1);
            s = s + " " + StringExpr(((InequProp*)p)->e2);
        }
        else if(((InequProp*)p)->p == GT){ 
            s = ">";
            s = s + " " + StringExpr(((InequProp*)p)->e1);
            s = s + " " + StringExpr(((InequProp*)p)->e2);
        }
        else{ 
            s = "=";
            s = s + " " + StringExpr(((InequProp*)p)->e1);
            s = s + " " + StringExpr(((InequProp*)p)->e2);
        }
    }
    else{
        s = "error";
    }
    return s;
}
string ART::StringPropWithTimes(Prop* p){
    string s;
    if(typeid(*p) == typeid(BoolProp)){
        if(((BoolProp*)p)->b == true){ s = "true"; }
        else{ s = "false"; }
    }
    else if(typeid(*p) == typeid(NegProp)){
        s = "~ ";
        s = s + StringPropWithTimes(((NegProp*)p)->p);
    }
    else if(typeid(*p) == typeid(BinProp)){
        s = StringLogicType(((BinProp*)p)->l);
        s = s + " " + StringPropWithTimes(((BinProp*)p)->p1);
        s = s + " " + StringPropWithTimes(((BinProp*)p)->p2);
    }
    else if(typeid(*p) == typeid(InequProp)){
        if(((InequProp*)p)->p == LT){
            s = "~ <=";
            s = s + " " + StringExprWithTimes(((InequProp*)p)->e2);
            s = s + " " + StringExprWithTimes(((InequProp*)p)->e1);
        }
        else if(((InequProp*)p)->p == GT){ 
            s = "~ <=";
            s = s + " " + StringExprWithTimes(((InequProp*)p)->e1);
            s = s + " " + StringExprWithTimes(((InequProp*)p)->e2);
        }
        else{ 
            s = "=";
            s = s + " " + StringExprWithTimes(((InequProp*)p)->e1);
            s = s + " " + StringExprWithTimes(((InequProp*)p)->e2);
        }
    }
    else{
        s = "error";
    }
    return s;
}

void PrintArtNodeS(ArtNode* artnode){
    if(typeid(*artnode) == typeid(BinArtNode)){
        cout << StringProp(((BinNode*)(((BinArtNode*)artnode)->cfa_node))->p); cout << endl;
    }
    else if(typeid(*artnode) == typeid(UniArtNode)){
        cout << "= ";
        cout << StringExpr(((UniNode*)(((UniArtNode*)artnode)->cfa_node))->e1);
        cout << " ";
        cout << StringExpr(((UniNode*)(((UniArtNode*)artnode)->cfa_node))->e2);
        cout << endl;
    }
    else if(typeid(*artnode) == typeid(BadArtNode)){
        cout << "BadNode!!!" << endl;
    }
    else if(typeid(*artnode) == typeid(TermArtNode)){
        cout << "TermNode!!!" << endl;
    }
    else{
    }
}
void ART::ChangeExpr(Expr* e1, int i1){
    pair<Expr*, int> sp;
    map<Expr*, int>::iterator it;
    if(typeid(*e1) == typeid(IntExpr)){    }
    else if(typeid(*e1) == typeid(VarExpr)){
        if(i1 == 0){
            //找到之後，加入新的Expr
            sp.first = e1;
            sp.second = 1;
            UseTimes.insert(sp);
        }
        else{
            it = UseTimes.find(e1);
            it->second = it->second + 1;
        }
    }
    else if(typeid(*e1) == typeid(ArrayExpr)){
        if(i1 == 0){
            sp.first = e1;
            sp.second = 1;
            UseTimes.insert(sp);
        }
        else{
            it = UseTimes.find(e1);
            it->second = it->second + 1;
        }
    }
    else if(typeid(*e1) == typeid(BinExpr)){
        ChangeExpr(((BinExpr*)e1)->e1, FindXTimes(((BinExpr*)e1)->e1));
        ChangeExpr(((BinExpr*)e1)->e2, FindXTimes(((BinExpr*)e1)->e2));
    }
}
string ART::PathFormula(ArtNode *N, int b){
    string s1, s2, s3;
    pair<Expr*, int> sp;
    map<Expr*, int>::iterator it;
    if(typeid(*N) == typeid(UniArtNode)){
        s2 = StringExprWithTimes(((UniNode*)((UniArtNode*)N)->cfa_node)->e2);
        ChangeExpr(((UniNode*)((UniArtNode*)N)->cfa_node)->e2, FindXTimes(((UniNode*)((UniArtNode*)N)->cfa_node)->e2));
        s1 = StringExprWithTimes(((UniNode*)((UniArtNode*)N)->cfa_node)->e1);
        ChangeExpr(((UniNode*)((UniArtNode*)N)->cfa_node)->e1, FindXTimes(((UniNode*)((UniArtNode*)N)->cfa_node)->e1));
        s3 = "= " + s1 + " " + s2;
    }
    else if(typeid(*N) == typeid(BinArtNode)){
        if(b == 1){                           //表示走左邊
            s3 = StringPropWithTimes(((BinNode*)(((BinArtNode*)N)->cfa_node))->p);
        }
        else if(b == -1){                     //表示走右邊
            Prop* neg;
            neg = new NegProp;
            ((NegProp*)neg)->p = ((BinNode*)(((BinArtNode*)N)->cfa_node))->p;
            s3 = StringPropWithTimes(neg);
        }
        else{
            s3 = "error!!";
        }
    }
    else if(typeid(*N) == typeid(BadArtNode)){
        s3 = "";
    }
    else if(typeid(*N) == typeid(TermArtNode)){
        cout << "TermNode" << endl;
        s3 = "";
    }
    else{
        s3 = "error";
    }
    return s3;
}
bool DFS(ArtNode* artnode, Node* cfanode, vector<ArtNode*> *path, vector<int> *path_b){
    if(artnode == 0){ return false; } 
    //cout << "Debug!!!!"; PrintArtNodeS(artnode);
    //CFA cfa;
    bool result;
    if(artnode->cfa_node == cfanode){
        path->push_back(artnode);
        return true;
    }
    else{
        if(typeid(*artnode) == typeid(BinArtNode)){
            //cout << "DFS BinNode1 "; cfa.PrintProp(((BinNode*)(((BinArtNode*)artnode)->cfa_node))->p); cout << endl;
            result = DFS(((BinArtNode*)artnode)->next1, cfanode, path, path_b);
            if(result == true){
                path->push_back(artnode);
                path_b->push_back(1);
                return result;
            }
            else{
                //cout << "DFS BinNode2 " << endl;
                result = DFS(((BinArtNode*)artnode)->next2, cfanode, path, path_b);
                if(result == true){
                    path->push_back(artnode);
                    path_b->push_back(-1);
                    return result;
                }
            }
        }
        else if(typeid(*artnode) == typeid(UniArtNode)){
            //cout << "DFS UniNode "; cfa.PrintExpr(((UniNode*)(((UniArtNode*)artnode)->cfa_node))->e1);
            //cout << "="; cfa.PrintExpr(((UniNode*)(((UniArtNode*)artnode)->cfa_node))->e2); cout << endl;
            result = DFS(((UniArtNode*)artnode)->next1, cfanode, path, path_b);
            if(result == true){
                path->push_back(artnode);
                path_b->push_back(0);
                return result;
            }
        }
        else if(typeid(*artnode) == typeid(BadArtNode)){
            //cout << "DFS BadNode " << endl;
            path->push_back(artnode);
            path_b->push_back(0);
            return true;
        }
        else if(typeid(*artnode) == typeid(TermArtNode)){
            //cout << "DFS TermNode " << endl;
            return false;
        }
        else{
            cout << "error" << endl;
        }
    }
    return false;
}
vector<Prop*> test1(){
    vector<Prop*> s;
    Prop *com, *k1, *k2;
    com = new BinProp;
    k1 = new InequProp;
    k2 = new InequProp;
    ((InequProp*)k1)->p = LT;
    ((InequProp*)k1)->e2 = new VarExpr;
    ((InequProp*)k1)->e1 = new IntExpr;
    strcpy(((VarExpr*)(((InequProp*)k1)->e2))->s, "x1");
    ((IntExpr*)(((InequProp*)k1)->e1))->i = 5;
    //cout << StringProp(k1) << endl;
    ((InequProp*)k2)->p = LT;
    ((InequProp*)k2)->e2 = new VarExpr;
    ((InequProp*)k2)->e1 = new IntExpr;
    strcpy(((VarExpr*)(((InequProp*)k2)->e2))->s, "x2");
    ((IntExpr*)(((InequProp*)k2)->e1))->i = 5;
    //cout << StringProp(k2) << endl;
    ((BinProp*)com)->p1 = k1;
    ((BinProp*)com)->p2 = k2;
    ((BinProp*)com)->l = And;
    //cout << StringProp(k2) << endl;
    s.push_back(k1);
    s.push_back(k2);
    return s;
}
vector<Prop*> test2(){
    int i1;
    i1 = 0;
    vector<Prop*> s;
    Prop **k1, **k2;
    k1 = new Prop* [10];
    k2 = new Prop* [10];
    for(i1 = 0; i1 < 10; i1++){
        k1[i1] = new InequProp;
        ((InequProp*)(k1[i1]))->e1 = new VarExpr;
        ((InequProp*)(k1[i1]))->e2 = new IntExpr;
        ((InequProp*)(k1[i1]))->p = Eq;
        strcpy(((VarExpr*)((InequProp*)(k1[i1]))->e1)->s, "x1");
        ((IntExpr*)((InequProp*)(k1[i1]))->e2)->i = i1;
        k2[i1] = new InequProp;
        ((InequProp*)(k2[i1]))->e1 = new VarExpr;
        ((InequProp*)(k2[i1]))->e2 = new IntExpr;
        ((InequProp*)(k2[i1]))->p = Eq;
        strcpy(((VarExpr*)((InequProp*)(k2[i1]))->e1)->s, "x2");
        ((IntExpr*)((InequProp*)(k2[i1]))->e2)->i = i1;
        s.push_back(k1[i1]);
        s.push_back(k2[i1]);
    }
    /*for(i1 = 0; i1 < 10; i1++){
        cout << "k1[" << i1 << "]="<< StringProp(k1[i1]) << endl;
        cout << "k2[" << i1 << "]="<< StringProp(k2[i1]) << endl;
    }*/
    return s;
}
vector<Prop*> test3(){
    vector<Prop*> s;
    Prop *com, *k1, *k2;
    com = new BinProp;
    k1 = new InequProp;
    k2 = new InequProp;
    ((InequProp*)k1)->p = LT;
    ((InequProp*)k1)->e2 = new VarExpr;
    ((InequProp*)k1)->e1 = new IntExpr;
    strcpy(((VarExpr*)(((InequProp*)k1)->e2))->s, "i1");
    ((IntExpr*)(((InequProp*)k1)->e1))->i = 5;
    //cout << StringProp(k1) << endl;
    ((InequProp*)k2)->p = LT;
    ((InequProp*)k2)->e2 = new VarExpr;
    ((InequProp*)k2)->e1 = new VarExpr;
    strcpy(((VarExpr*)(((InequProp*)k2)->e2))->s, "i2");
    strcpy(((VarExpr*)(((InequProp*)k2)->e1))->s, "i3");
    //cout << StringProp(k2) << endl;
    ((BinProp*)com)->p1 = k1;
    ((BinProp*)com)->p2 = k2;
    ((BinProp*)com)->l = And;
    //cout << StringProp(k2) << endl;
    s.push_back(k1);
    s.push_back(k2);
    return s;
}
void ART::CFA2ART(CFA *cfa){
    int i1;
    i1 = 0;
    set<int> s;
    bool result;
    vector<ArtNode*> path;
    vector<int> path_b;
    call_time = 0;
    //read CFA initial Node
    Node* n;
    ArtNode *artNode;
    artNode = NULL;
    Prop *initPred, *initPhi;
    initPred = new BoolProp;
    initPhi = new BoolProp;
    ((BoolProp*)initPred)->b = true;
    
    ((BoolProp*)initPhi)->b = true;
    n = cfa->GetInitNode();
    if(typeid(*n) == typeid(UniNode)){
        artNode = new UniArtNode;
        ((UniArtNode*)artNode)->cfa_node = n;
    }
    else if(typeid(*n) == typeid(UniNode)){
        artNode = new BinArtNode;
        ((UniArtNode*)artNode)->cfa_node = n;
    }
    else if(typeid(*n) == typeid(BadNode)){ 
        artNode = new BadArtNode;
        ((BadArtNode*)artNode)->cfa_node = n;
    }
    else if(typeid(*n) == typeid(BadNode)){
        artNode = new TermArtNode;
        ((TermArtNode*)artNode)->cfa_node = n;
    }
    else{ }
    //artNode->predicate.push_back(initPred);		//這個是init predicate
    //artNode->predicate = test1(); 			//這個是ninenine.txt
    //artNode->predicate = test2();			//這個是ninenine.txt
    artNode->predicate = test3();			//這個是pascal.txt
    //cout << StringProp((artNode->predicate)[0]) << endl;
    //cout << StringProp((artNode->predicate)[1]) << endl;
    artNode->phi = initPhi;
    try{
       BuildART(artNode);
    }
    catch(bad_alloc err){
        cout << err.what() << endl;
    }
    result = DFS(artNode, NULL, &path, &path_b);
    if(result == true){ 
        for(i1 = path.size()-1; i1 >= 0; i1--){
            //PrintArtNodeS(path[i1]);
            cout << PathFormula(path[i1], path_b[i1]);
            if(i1 > 1){
                cout << " ;" << endl;
            }
            else{
                cout << endl;
            }
        }
    }
    else{ cout << "system safe" << endl; }
    //PathFormula(artNode);
    //PrintArtNode(artNode);
    //RecursiveBuildArt(cfa->GetInitNode(), &s);
}
